L:Dsys List.
(A,BL.interface-compatible(A;B))  (A,BL.A || B)  (AL. Feasible(A))  Feasible((L)) 

latex

Definitions	(L), Feasible(D), Dsys, xL. P(x), P  Q, A || B, (x,yL.P(x;y)), interface-compatible(A;B), System, type List, x:A. B(x), t  T, x:AB(x), nil, ||as||, P & Q, i  j < k, a<b, False, A, AB, , {x:A| B(x) }, {i..j}, #$n, Void, MsgA, Id, Type, l[i], Prop, x. t(x), x:AB(x), a:A fp B(a), , Atom, , car.cdr, S  T, x.A(x), P  Q, x,y. t(x;y), f(a), Feasible(M), T, True, {T}, M(i), s = t
Lemmas	m-sys-join-list-property2, m-sys-join-list-property, ma-feasible wf, m-sys-feasible-join, m-sys-join-list wf2, m-sys-join-list wf, pairwise wf, pairwise-cons, l all cons, d-feasible-null, l all wf, d-feasible wf, dsys wf, m-sys-compatible wf, int seg wf, interface-compatible wf, select wf, Id wf, msga wf, length wf2, msystem wf